#!/usr/bin/env ruby

require 'enumerator'

DBC_SUFFIX = "__dbc_internal__"

def gen_checks(dbc_conf, def_line)
    def_line =~ /^(.+?)#{dbc_conf[:name]}(.+)$/ or fail "function definition does not match dbc-name\nDetails:\n\tdbc-name = #{dbc_conf[:name]}\n\tdefinition: '#{def_line.strip}'\n"
    new_def_line = "%s%s%s" % [$1, dbc_conf[:name] + DBC_SUFFIX, $2]

    puts "#{new_def_line};"
    
    puts "#{dbc_conf[:return]} #{dbc_conf[:name]} (#{dbc_conf[:arg].enum_with_index.map { |type, i| "#{type} a#{i}"}.join(', ')})"
    puts "{"
    puts "  #{dbc_conf[:return]} ret;" if dbc_conf[:return]
    dbc_conf[:pre].each do |pre|
	puts %Q|  assert (#{pre.gsub(/#arg(\d+)/) {"a#$1"}} && "pre-condition violation in #{dbc_conf[:name]} '#{pre}'");|
    end
    print "  ret = " if dbc_conf[:return]
    puts "   #{dbc_conf[:name] + DBC_SUFFIX} (#{Enumerable::Enumerator.new(dbc_conf[:arg].length, :times).map { |i| "a#{i}"}.join(', ')});"
    dbc_conf[:post].each do |post|
	puts %Q|  assert (#{post.gsub(/#arg(\d+)/) {"a#$1"}.gsub('#ret','ret')} && "post-condition violation in #{dbc_conf[:name]} '#{post}'");|
    end
    puts "  return ret;" if dbc_conf[:return]
    puts "}"
    puts
    puts new_def_line
end

puts "#include <assert.h>"
while line = gets
    case line
    when /@name\s+(.+)/
	dbc_conf = {:name => $1.strip, :arg => [], :pre => [], :post => []}
    when /@return\s+(.+)/
	dbc_conf[:return] = $1.strip
    when /@arg\s+(\d+)\s+(.+)/
	dbc_conf[:arg][$1.to_i] = $2.strip
    when /@(pre|post)\s+(.+)/
	kind = $1.to_sym
	dbc_conf[kind] << $2.strip
    when /@dbc@/
	gen_checks(dbc_conf, line)
    else
	print line
    end
end
